/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model.game;

import com.sun.org.apache.xalan.internal.xsltc.runtime.Hashtable;
import java.io.IOException;
import java.util.Iterator;
import java.util.Vector;
/*import jdd.JDD;
import jdd.JDDNode;*/

/**
 * WARNING : not used anymore
 *
 *
 * This class represent the two bdd of the game. The bdd for player 1 and the bdd
 * for player 2. The structure of the boolean formula on the bdd is :
 * source + atomicProposition + target on bit representation
 */

/**
 *
 * @author simon
 */
//public class BddDecoration extends GameDecorator {


    /*private int nbreByteNodeP1_;
    private int nbreByteNodeP2_;
    //Represent the number of bytes necessary for represent all the nodes of automata
    private int nbreByteAlphabet_;
    //Represent the number of bytes necessary for represent all the alphabet
    private int sizeBooleanFormulaP1_;
    private int sizeBooleanFormulaP2_;
    //Represent the size of a boolean formula for represent a transition
    private jdd.JDDNode bddPlayer1_;
    private jdd.JDDNode bddPlayer2_;
    private Vector<Boolean[]> transPlayer1_;
    private Vector<Boolean[]> transPlayer2_;
    private Hashtable bitNodeP1_;
    private Hashtable bitNodeP2_;
    //correspondance between the name of a node and his bit representation
    private Hashtable atomicProp_;
    private Vector<JDDNode> bddVariables_;


    public BddDecoration(){
        super(Tag.BDD);
        bitNodeP1_ = new Hashtable();
        bitNodeP2_ = new Hashtable();
        atomicProp_ = new Hashtable();
        transPlayer1_ = new Vector<Boolean[]>();
        transPlayer2_ = new Vector<Boolean[]>();
    }

    public int getNbreByteNode(int player){
        if (player == 1)
            return nbreByteNodeP1_;
        else
            return nbreByteNodeP2_;
    }

    public int getNbreByteAlphabet(){
        return nbreByteAlphabet_;
    }

    public JDDNode getBddPlayer1(){
        return bddPlayer1_;
    }

    public JDDNode getBddPlayer2(){
        return bddPlayer2_;
    }

    public boolean[] getNode (int name, int player){
        if (player == 1)
            return (boolean[]) bitNodeP1_.get(name);
        else
            return (boolean[]) bitNodeP2_.get(name);
    }

    public int getSizeFormula(int player){
        if (player == 1)
            return getSizeFormulaP1();
        else
            return getSizeFormulaP2();
    }

    public int getSizeFormulaP1(){
        return sizeBooleanFormulaP1_;
    }

    public int getSizeFormulaP2(){
        return sizeBooleanFormulaP2_;
    }

    public void addNode(int name, boolean[] representation, int player){
        if (player==1)
            bitNodeP1_.put(name, representation);
        else
            bitNodeP2_.put(name,representation);
        //the number of the node, his name, is associated to his bit value in automata.
        /*System.out.print("add "+name+" : ");
        for (int i=0; i<representation.length; ++i)
            if (representation[i])
                System.out.print("1");
            else
                System.out.print("0");
        System.out.println();*/
   // }

   /* public void addAtomicProposition(String name, int value){
        atomicProp_.put(name, value);
    }

    public void setNbreBitNode(int nbre, int player){
        if (player == 1 )
            nbreByteNodeP1_ = nbre;
        else
            nbreByteNodeP2_ = nbre;
    }

    public void setNbreByteAlphabet(int nbre){
        nbreByteAlphabet_ = nbre;
    }

    public void setSizeBooleanFormula(int size, int player){
        if (player == 1)
            sizeBooleanFormulaP1_ = size;
        else
            sizeBooleanFormulaP2_ = size;
    }

    public void addTrans (int player, Vector<Boolean[]> trans) throws IOException{
        if (player == 1){
            transPlayer1_ = new Vector<Boolean[]>();
            transPlayer1_=(trans);
        }
        else if (player == 2){
            transPlayer2_ = new Vector<Boolean[]>();
            transPlayer2_=(trans);
        }
        else
            throw new IOException("Unknow player");
    }

    public Integer getAtomicProposition(String name){
        return (Integer) atomicProp_.get(name);
    }

    //This method convert the transition structure (symbolic bdd) to a bdd
    public void createBDD(int player){
        if (player==1)
            bddPlayer1_ = createBDD(transPlayer1_,1);
        else
            bddPlayer2_ = createBDD(transPlayer2_,2);
    }

    private JDDNode createBDD(Vector<Boolean[]> transPlayer, int player) {
        /** The formula is an Or combinaison of all the transition.
         * The formula that represent a transition is a conjuction of all
         * the boolean.
         */

        /* System.out.println(transPlayer.get(0));
       JDD.InitialiseCUDD();

       Vector<JDDNode> trans = new Vector<JDDNode>();

       //creation of all the transition formula
       Iterator iter = transPlayer.iterator();

       //First step creation of the variables
       int nbreVar = getSizeFormula(player);
       bddVariables_ = new Vector<JDDNode>();
       for (int i=0; i < nbreVar; ++i)
           bddVariables_.add(JDD.Var(i));

       //second step creation of the BDD
       
       while (iter.hasNext()){
           trans.add(createTransitionFormula(bddVariables_,(Boolean[]) iter.next()));
       }

       //Third step : create the BDD
       JDDNode state;
       if (trans.size() == 1){
           state = trans.get(0);
           JDD.Ref(state);
       }
       else if (trans.size() > 1){
           state = JDD.Or(trans.get(0), trans.get(1));
           JDD.Ref(state);

           for (int i=2; i < trans.size(); ++i){
               JDDNode newState = JDD.Or(state, trans.get(i));
               JDD.Deref(state);
               state = newState;
               JDD.Ref(state);
           }

       }
       else
           state = null;

       //System.out.println("bdd info : "+JDD.GetInfoString(state, nbreVar));

       return state;
    }

    private JDDNode createTransitionFormula(Vector<JDDNode> var, Boolean[] formula) {
        //Creation of the first node
        JDDNode state = getNode(var,formula[0],formula[1]);
        JDD.Ref(state);
        for (int i=2; i < formula.length; ++i){
            JDDNode newState = getNode(var,i,state,formula[i]);
            JDD.Deref(state);
            state = newState;
            JDD.Ref(state);
        }
        return state;
    }


    //Return the inital node of the bdd
    private JDDNode getNode(Vector<JDDNode> var, Boolean b0, Boolean b1) {
        if (b0 && b1)
            return JDD.And(var.get(0), var.get(1));
        else if (b0 &&!b1)
            return JDD.And(var.get(0), JDD.Not(var.get(1)));
        else if (!b0 && !b1)
            return JDD.And(JDD.Not(var.get(0)), JDD.Not(var.get(1)));
        else
            return JDD.And(JDD.Not(var.get(0)), var.get(1));
    }

    private JDDNode getNode(Vector<JDDNode> var, int i, JDDNode state, Boolean b) {
        if (b)
            return JDD.And(state, var.get(i));
        else
            return JDD.And(state, JDD.Not(var.get(i)));
    }*/

//}
